(declare-sort S0 0)

(declare-sort S1 0)

(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const i0 Int)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const r2 Real)
(declare-const r5 Real)
(declare-const r7 Real)
(declare-const v19 Bool)
(declare-const r8 Real)
(check-sat)
(declare-const arr--6460741003321626144_-348611824890845743-0 (Array Real (_ BitVec 12)))
(assert (not (forall ((q0 S0) (q1 Real)) v6)))
(assert (or (forall ((q0 S0) (q1 Real)) (=> (= q0 q0 q0 q0) (distinct (to_real i4) r8))) (exists ((q0 S0) (q1 Real)) (not (= q0 q0 q0)))))
(assert v1)
(push)
(declare-const r9 Real)
(check-sat)
(pop)
(declare-const v20 Bool)
(assert (exists ((q2 (_ BitVec 12)) (q3 Bool) (q4 Real)) (not (bvult #x1e8 #x1e8))))
(assert v18)
(check-sat)
(push)
(declare-const arr--348611824894093318_-348611824890845743-0 (Array (_ BitVec 9) (_ BitVec 12)))
(assert (= v16 v11 v11 v0 (distinct 88 i4) v4 v2))
(pop)
(declare-const _17-0 (_ BitVec 17))
(check-sat)
